package edu.uclm.combTest.core.pairwise;

/**
 * Une paire. Les indices a et b sont les position de l'élément dans le tableau
 * des éléments d'un paramettre.
 * 
 * @author quentin
 * 
 */
public class Pair {
	protected/*@ spec_public @*/int a;
	protected/*@ spec_public @*/int b;
	/**
	 * Nombre de visite de la pair.
	 */
	protected/*@ spec_public @*/int weight;

	//@ public invariant weight >=0;
	//@ public invariant a >= 0;
	//@ public invariant b >= 0;

	// Le nombre de visite d'une Pair peut augmenter mais pas diminuer.
	//@ public constraint weight == \old(weight) || weight == \old(weight)+1 ;

	//@requires a >= 0 ;
	//@requires b >=0;
	//@ensures weight==0;
	public Pair(int a, int b) {
		this.a = a;
		this.b = b;
		this.weight = 0;
	}

	public/*@ pure @*/String toString() {
		return "(" + a + ", " + b + ") -> " + this.weight;
	}

	//@ensures \result == weight;
	public/*@ pure @*/int weight() {
		return this.weight;
	}

	//@ensures \result == a;
	public/*@ pure @*/int getA() {
		return a;
	}

	//@ensures \result==b;
	public/*@ pure @*/int getB() {
		return b;
	}

	//@ensures weight == \old(weight)+1 ;
	public void increaseWeight() {
		this.weight = weight + 1;
	}
	
	/**
	 * Egale si désigne la même pair, avec potentiellement une taille diférente.
	 */
	public/*@ pure @*/  boolean equals(/*@ nullable @*/Object obj) {
		
		if((obj == null)||( ! (obj instanceof Pair)))
			return false;
		Pair p = (Pair)obj;
		return a == p.getA() && b == p.getB();
		
	}

}
